pnueli-zuck.5.jani:model: info: pnueli-zuck.5 is an MDP model.
pnueli-zuck.5.jani:variables[0]: info: Expanding variable "p0" into 16 locations in automaton "process0".
pnueli-zuck.5.jani:variables[1]: info: Expanding variable "p1" into 16 locations in automaton "process1".
pnueli-zuck.5.jani:variables[2]: info: Expanding variable "p2" into 16 locations in automaton "process2".
pnueli-zuck.5.jani:variables[3]: info: Expanding variable "p3" into 16 locations in automaton "process3".
pnueli-zuck.5.jani:variables[4]: info: Expanding variable "p4" into 16 locations in automaton "process4".
pnueli-zuck.5.jani: info: Need 16 bytes per state.
pnueli-zuck.5.jani: info: Explored 307523 states.
Peak memory usage: 291 MB
Analysis results for pnueli-zuck.5.jani
+ State space exploration
State size: 16 bytes
States: 307523
Transitions: 1753715
Branches: 1886851
Rate: 196878 states/s
Time: 1.7 s
+ Property live
Probability: 1
Bounds: [1, 1]
Time: 1.3 s
+ Essential states
Iterations: 1
Essential states: 303428
Transitions: 1749620
Branches: 1882756
Time: 0.1 s
+ Optimistic value iteration
Total iterations: 37
Verif. attempts: 1
Verif. iterations: 1
Final epsilon: 1E-06
Time: 1.1 s
Exported results to file "/out.txt".